$\forall$${\it es}$:ES, $A$:Type, $f$:Top, ${\it Ia}$:AbsInterface($A$), $e$:E. ($\uparrow$($e$ $\in_{b}$ ${\it Ia}$)) $\Rightarrow$ ($f$'${\it Ia}$($e$) $\sim$ ($f$(${\it Ia}$($e$))))